(declare-fun value1 () String)
(declare-fun value2 () String)
(assert (or (and (not (str.contains value2 "J")) (str.contains value2 "I") (not (= (ite (str.contains value2 "H") 1 0) (ite (str.contains value2 "GF") 1 0) 0)) (not (= (ite (str.contains value2 "E") 1 0) 0)) (not (= (ite (str.contains value2 "D") 1 0) 0)) (not (= (ite (str.contains value2 "B") 1 0) (ite (str.contains value2 "A") 1 0) 0))) (not (= (str.at value2 (- (str.len value2) 1)) "u;"))))
(assert (not (= (str.at value2 0) "ub")))
(assert (not (= (str.at value2 0) "u9")))
(assert (not (= (str.at value2 0) "c")))
(assert (= (str.indexof value2 "=" 0) 1))
(assert (= (ite (str.contains value2 ",") 1 0) (ite (= (str.len value2) 0) 1 0) 0))
(assert (>= (* (str.len value1) (str.indexof value1 "=" 0)) (- (str.indexof (str.substr value1 0 (str.indexof value1 "=" 0)) "L" 0) 1) 0))
(check-sat)
